(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Rewrite Strategy: FULL
(1) CpxTrsToCpxRelTrsProof (BOTH BOUNDS(ID, ID) transformation)
Transformed TRS to relative TRS where S is empty.
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
S is empty.
Rewrite Strategy: FULL
(3) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(2n):
The rewrite sequence
activate(n__s(n__div(n__s(X29820_3), n__s(Y30785_3)))) →+ s(if(geq(activate(X29820_3), activate(Y30785_3)), n__s(n__div(n__minus(activate(X29820_3), activate(Y30785_3)), n__s(activate(Y30785_3)))), n__0))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0,0].
The pumping substitution is [X29820_3 / n__s(n__div(n__s(X29820_3), n__s(Y30785_3)))].
The result substitution is [ ].
The rewrite sequence
activate(n__s(n__div(n__s(X29820_3), n__s(Y30785_3)))) →+ s(if(geq(activate(X29820_3), activate(Y30785_3)), n__s(n__div(n__minus(activate(X29820_3), activate(Y30785_3)), n__s(activate(Y30785_3)))), n__0))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1,0,0,0].
The pumping substitution is [X29820_3 / n__s(n__div(n__s(X29820_3), n__s(Y30785_3)))].
The result substitution is [ ].
(4) BOUNDS(2^n, INF)